`timescale 1ns/1ps

module async_fifo_props(
    input         rclk,
    input         wclk,
    input         rst_n,
    input         wr_en,
    input         rd_en,
    input [7:0]   wr_data,
    input [7:0]   rd_data,
    input         empty,
    input         full
);

// 实例化被测设计
async_fifo u_fifo (
    .rclk(rclk),
    .wclk(wclk),
    .rst_n(rst_n),
    .wr_en(wr_en),
    .rd_en(rd_en),
    .wr_data(wr_data),
    .rd_data(rd_data),
    .empty(empty),
    .full(full)
);

always @(posedge wclk) begin
    if(wr_en && !full) begin
        assert(u_fifo.wr_ptr == $past(u_fifo.wr_ptr) + 1);
    end
end

// 空信号冲突检测
always @(posedge rclk) begin
    if(!empty && (u_fifo.rd_ptr >= u_fifo.wr_ptr)) begin
        $display("[ERROR] Pointers conflict: rd=%0d wr=%0d",u_fifo.rd_ptr, u_fifo.wr_ptr);
    end
end

endmodule